@Article{SantosErasSantVija:2014:FoVeTo,
               author = "Santos, Luciana Brasil Rebelo dos and Eras, Eduardo Rohde and 
                         Santiago Jr., Valdivino Alexandre de and Vijaykumar, Nandamudi 
                         Lankalapalli",
          affiliation = "{Instituto Nacional de Pesquisas Espaciais (INPE)} and {Instituto 
                         Nacional de Pesquisas Espaciais (INPE)} and {Instituto Nacional de 
                         Pesquisas Espaciais (INPE)} and {Instituto Nacional de Pesquisas 
                         Espaciais (INPE)}",
                title = "A formal verification tool for UML behavioral diagrams",
              journal = "Lecture Notes in Computer Science",
                 year = "2014",
               volume = "8579 LNCS",
               number = "PART 1",
                pages = "696--711",
             keywords = "Model checking, Behavioral diagrams, Formal verification tools, 
                         Formal verifications, Modeling behavior, Object oriented software, 
                         Software model checking, State machine, Transition system, Unified 
                         Modeling Language.",
             abstract = "Unified Modeling Language (UML) is considered a standard for 
                         modeling object-oriented software. It supports several different 
                         diagrams that can be used to model behavior and structure of the 
                         software. With respect to formal verification, particularly Model 
                         Checking, the existing approaches are usually restricted to a 
                         single UML diagram. This paper presents a tool to convert UML 
                         behavioral diagrams (sequence, activity, and state machine) into 
                         Transition Systems to support software Model Checking. A peculiar 
                         feature of our tool is that it is developed as part of a larger 
                         effort to allow Model Checking of software built in accordance 
                         with UML, including several UML behavioral diagrams. We 
                         demonstrate the effectiveness of our approach by applying it to a 
                         classic case study and also to a real case study (embedded 
                         software) in the space domain. © 2014 Springer International 
                         Publishing.",
                  doi = "10.1007/978-3-319-09144-0_48",
                  url = "http://dx.doi.org/10.1007/978-3-319-09144-0_48",
                 isbn = "9783319091433",
                 issn = "0302-9743",
                label = "scopus 2014-11 DosSantosErasSantVija:2014:FoVeTo",
             language = "en",
        urlaccessdate = "27 abr. 2024"
}